app(app(and, true), true) → true
app(app(and, x), false) → false
app(app(and, false), y) → false
app(app(or, true), y) → true
app(app(or, x), true) → true
app(app(or, false), false) → false
app(app(forall, p), nil) → true
app(app(forall, p), app(app(cons, x), xs)) → app(app(and, app(p, x)), app(app(forall, p), xs))
app(app(forsome, p), nil) → false
app(app(forsome, p), app(app(cons, x), xs)) → app(app(or, app(p, x)), app(app(forsome, p), xs))
↳ QTRS
↳ DependencyPairsProof
app(app(and, true), true) → true
app(app(and, x), false) → false
app(app(and, false), y) → false
app(app(or, true), y) → true
app(app(or, x), true) → true
app(app(or, false), false) → false
app(app(forall, p), nil) → true
app(app(forall, p), app(app(cons, x), xs)) → app(app(and, app(p, x)), app(app(forall, p), xs))
app(app(forsome, p), nil) → false
app(app(forsome, p), app(app(cons, x), xs)) → app(app(or, app(p, x)), app(app(forsome, p), xs))
APP(app(forsome, p), app(app(cons, x), xs)) → APP(or, app(p, x))
APP(app(forsome, p), app(app(cons, x), xs)) → APP(p, x)
APP(app(forall, p), app(app(cons, x), xs)) → APP(app(and, app(p, x)), app(app(forall, p), xs))
APP(app(forsome, p), app(app(cons, x), xs)) → APP(app(or, app(p, x)), app(app(forsome, p), xs))
APP(app(forall, p), app(app(cons, x), xs)) → APP(app(forall, p), xs)
APP(app(forall, p), app(app(cons, x), xs)) → APP(p, x)
APP(app(forsome, p), app(app(cons, x), xs)) → APP(app(forsome, p), xs)
APP(app(forall, p), app(app(cons, x), xs)) → APP(and, app(p, x))
app(app(and, true), true) → true
app(app(and, x), false) → false
app(app(and, false), y) → false
app(app(or, true), y) → true
app(app(or, x), true) → true
app(app(or, false), false) → false
app(app(forall, p), nil) → true
app(app(forall, p), app(app(cons, x), xs)) → app(app(and, app(p, x)), app(app(forall, p), xs))
app(app(forsome, p), nil) → false
app(app(forsome, p), app(app(cons, x), xs)) → app(app(or, app(p, x)), app(app(forsome, p), xs))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
APP(app(forsome, p), app(app(cons, x), xs)) → APP(or, app(p, x))
APP(app(forsome, p), app(app(cons, x), xs)) → APP(p, x)
APP(app(forall, p), app(app(cons, x), xs)) → APP(app(and, app(p, x)), app(app(forall, p), xs))
APP(app(forsome, p), app(app(cons, x), xs)) → APP(app(or, app(p, x)), app(app(forsome, p), xs))
APP(app(forall, p), app(app(cons, x), xs)) → APP(app(forall, p), xs)
APP(app(forall, p), app(app(cons, x), xs)) → APP(p, x)
APP(app(forsome, p), app(app(cons, x), xs)) → APP(app(forsome, p), xs)
APP(app(forall, p), app(app(cons, x), xs)) → APP(and, app(p, x))
app(app(and, true), true) → true
app(app(and, x), false) → false
app(app(and, false), y) → false
app(app(or, true), y) → true
app(app(or, x), true) → true
app(app(or, false), false) → false
app(app(forall, p), nil) → true
app(app(forall, p), app(app(cons, x), xs)) → app(app(and, app(p, x)), app(app(forall, p), xs))
app(app(forsome, p), nil) → false
app(app(forsome, p), app(app(cons, x), xs)) → app(app(or, app(p, x)), app(app(forsome, p), xs))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
APP(app(forsome, p), app(app(cons, x), xs)) → APP(p, x)
APP(app(forall, p), app(app(cons, x), xs)) → APP(p, x)
APP(app(forall, p), app(app(cons, x), xs)) → APP(app(forall, p), xs)
APP(app(forsome, p), app(app(cons, x), xs)) → APP(app(forsome, p), xs)
app(app(and, true), true) → true
app(app(and, x), false) → false
app(app(and, false), y) → false
app(app(or, true), y) → true
app(app(or, x), true) → true
app(app(or, false), false) → false
app(app(forall, p), nil) → true
app(app(forall, p), app(app(cons, x), xs)) → app(app(and, app(p, x)), app(app(forall, p), xs))
app(app(forsome, p), nil) → false
app(app(forsome, p), app(app(cons, x), xs)) → app(app(or, app(p, x)), app(app(forsome, p), xs))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
APP(app(forsome, p), app(app(cons, x), xs)) → APP(p, x)
APP(app(forall, p), app(app(cons, x), xs)) → APP(p, x)
APP(app(forall, p), app(app(cons, x), xs)) → APP(app(forall, p), xs)
APP(app(forsome, p), app(app(cons, x), xs)) → APP(app(forsome, p), xs)
The value of delta used in the strict ordering is 12.
POL(APP(x1, x2)) = (2)x_1 + x_2
POL(cons) = 3
POL(forall) = 2
POL(app(x1, x2)) = (2)x_1 + x_2
POL(forsome) = 4
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
app(app(and, true), true) → true
app(app(and, x), false) → false
app(app(and, false), y) → false
app(app(or, true), y) → true
app(app(or, x), true) → true
app(app(or, false), false) → false
app(app(forall, p), nil) → true
app(app(forall, p), app(app(cons, x), xs)) → app(app(and, app(p, x)), app(app(forall, p), xs))
app(app(forsome, p), nil) → false
app(app(forsome, p), app(app(cons, x), xs)) → app(app(or, app(p, x)), app(app(forsome, p), xs))